1  (∀N.((0≥N∧Q(N))⊃∃N1.(Q(N1)∧∀M.(¬(M≥N1)⊃¬Q(M))))∧∀N.(∀N2.((N≥N2∧Q(N2))⊃∃N1.(Q(N1)∧∀M.(¬(M≥N1)⊃¬Q(M))))⊃∀N2.((S%
UCCN≥N2∧Q(N2))⊃∃N1.(Q(N1)∧∀M.(¬(M≥N1)⊃¬Q(M))))))⊃∀N N2.((N≥N2∧Q(N2))⊃∃N1.(Q(N1)∧∀M.(¬(M≥N1)⊃¬Q(M))))    ∧I (NIL)%
 

2  M≥0    ∀E NIL M 

3  ¬(M≥0)⊃¬Q(M)    TAUT 

4  ∀M.(¬(M≥0)⊃¬Q(M))    ∀I 3 M ← M 

5  Q(0)  (5)  ASSUME 

6  Q(0)∧∀M.(¬(M≥0)⊃¬Q(M))  (5)  ∧I (5 4) 

7  ∃N1.(Q(N1)∧∀M.(¬(M≥N1)⊃¬Q(M)))  (5)  6 0 ← N1 

8  0≥N⊃N=0    ∀E NIL N 

9  Q(0)⊃∃N1.(Q(N1)∧∀M.(¬(M≥N1)⊃¬Q(M)))    ⊃I 5 7 

10  (0≥N∧Q(N))⊃∃N1.(Q(N1)∧∀M.(¬(M≥N1)⊃¬Q(M)))    TAUTEQ 

11  ∀N.((0≥N∧Q(N))⊃∃N1.(Q(N1)∧∀M.(¬(M≥N1)⊃¬Q(M))))    ∀I 10 N ← N 

12  ∀N.(∀N2.((N≥N2∧Q(N2))⊃∃N1.(Q(N1)∧∀M.(¬(M≥N1)⊃¬Q(M))))⊃∀N2.((SUCCN≥N2∧Q(N2))⊃∃N1.(Q(N1)∧∀M.(¬(M≥N1)⊃¬Q(M)))))%
⊃∀N N2.((N≥N2∧Q(N2))⊃∃N1.(Q(N1)∧∀M.(¬(M≥N1)⊃¬Q(M))))    TAUT 

13  ∀N2.((N≥N2∧Q(N2))⊃∃N1.(Q(N1)∧∀M.(¬(M≥N1)⊃¬Q(M))))  (13)  ASSUME 

14  Q(SUCCN)  (14)  ASSUME 

15  ∀M.(¬(M≥SUCCN)⊃¬Q(M))  (15)  ASSUME 

16  Q(SUCCN)∧∀M.(¬(M≥SUCCN)⊃¬Q(M))  (14 15)  ∧I (14 15) 

17  ∃N1.(Q(N1)∧∀M.(¬(M≥N1)⊃¬Q(M)))  (14 15)  16 SUCCN ← N1